r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
↳ QTRS
↳ DependencyPairsProof
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
B(ql(1(x1))) → R1(x1)
B(ql(1(x1))) → B(r1(x1))
R0(1(x1)) → 11(r0(x1))
R0(m(x1)) → R0(x1)
01(ql(x1)) → 01(x1)
R1(m(x1)) → M(r1(x1))
B(ql(0(x1))) → R0(x1)
M(qr(x1)) → M(x1)
B(ql(1(x1))) → 11(b(r1(x1)))
R0(b(x1)) → 01(b(x1))
R0(m(x1)) → M(r0(x1))
R0(1(x1)) → R0(x1)
B(ql(0(x1))) → 01(b(r0(x1)))
B(ql(0(x1))) → B(r0(x1))
R1(b(x1)) → 11(b(x1))
R1(1(x1)) → R1(x1)
R0(0(x1)) → R0(x1)
R1(m(x1)) → R1(x1)
R1(0(x1)) → 01(r1(x1))
11(qr(x1)) → 11(x1)
R1(0(x1)) → R1(x1)
R0(0(x1)) → 01(r0(x1))
11(ql(x1)) → 11(x1)
R1(1(x1)) → 11(r1(x1))
01(qr(x1)) → 01(x1)
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
B(ql(1(x1))) → R1(x1)
B(ql(1(x1))) → B(r1(x1))
R0(1(x1)) → 11(r0(x1))
R0(m(x1)) → R0(x1)
01(ql(x1)) → 01(x1)
R1(m(x1)) → M(r1(x1))
B(ql(0(x1))) → R0(x1)
M(qr(x1)) → M(x1)
B(ql(1(x1))) → 11(b(r1(x1)))
R0(b(x1)) → 01(b(x1))
R0(m(x1)) → M(r0(x1))
R0(1(x1)) → R0(x1)
B(ql(0(x1))) → 01(b(r0(x1)))
B(ql(0(x1))) → B(r0(x1))
R1(b(x1)) → 11(b(x1))
R1(1(x1)) → R1(x1)
R0(0(x1)) → R0(x1)
R1(m(x1)) → R1(x1)
R1(0(x1)) → 01(r1(x1))
11(qr(x1)) → 11(x1)
R1(0(x1)) → R1(x1)
R0(0(x1)) → 01(r0(x1))
11(ql(x1)) → 11(x1)
R1(1(x1)) → 11(r1(x1))
01(qr(x1)) → 01(x1)
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
M(qr(x1)) → M(x1)
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
M(qr(x1)) → M(x1)
The value of delta used in the strict ordering is 4.
POL(qr(x1)) = 1 + (4)x_1
POL(M(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
11(qr(x1)) → 11(x1)
11(ql(x1)) → 11(x1)
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
11(qr(x1)) → 11(x1)
11(ql(x1)) → 11(x1)
The value of delta used in the strict ordering is 16.
POL(11(x1)) = (4)x_1
POL(qr(x1)) = 4 + x_1
POL(ql(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
01(ql(x1)) → 01(x1)
01(qr(x1)) → 01(x1)
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
01(ql(x1)) → 01(x1)
01(qr(x1)) → 01(x1)
The value of delta used in the strict ordering is 16.
POL(01(x1)) = (4)x_1
POL(ql(x1)) = 4 + x_1
POL(qr(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
R1(0(x1)) → R1(x1)
R1(1(x1)) → R1(x1)
R1(m(x1)) → R1(x1)
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R1(0(x1)) → R1(x1)
R1(1(x1)) → R1(x1)
R1(m(x1)) → R1(x1)
The value of delta used in the strict ordering is 16.
POL(1(x1)) = 4 + (4)x_1
POL(m(x1)) = 4 + (4)x_1
POL(R1(x1)) = (4)x_1
POL(0(x1)) = 4 + (3)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
R0(1(x1)) → R0(x1)
R0(0(x1)) → R0(x1)
R0(m(x1)) → R0(x1)
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R0(1(x1)) → R0(x1)
R0(0(x1)) → R0(x1)
R0(m(x1)) → R0(x1)
The value of delta used in the strict ordering is 16.
POL(1(x1)) = 4 + (4)x_1
POL(m(x1)) = 4 + (3)x_1
POL(R0(x1)) = (4)x_1
POL(0(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
B(ql(1(x1))) → B(r1(x1))
B(ql(0(x1))) → B(r0(x1))
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
B(ql(1(x1))) → B(r1(x1))
Used ordering: Polynomial interpretation [25,35]:
B(ql(0(x1))) → B(r0(x1))
The value of delta used in the strict ordering is 8.
POL(r0(x1)) = x_1
POL(1(x1)) = 4 + (2)x_1
POL(m(x1)) = 0
POL(B(x1)) = (2)x_1
POL(ql(x1)) = x_1
POL(qr(x1)) = 0
POL(b(x1)) = 2 + (4)x_1
POL(r1(x1)) = x_1
POL(0(x1)) = x_1
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
b(ql(1(x1))) → 1(b(r1(x1)))
r0(1(x1)) → 1(r0(x1))
r0(0(x1)) → 0(r0(x1))
r1(0(x1)) → 0(r1(x1))
r0(m(x1)) → m(r0(x1))
r1(m(x1)) → m(r1(x1))
r1(1(x1)) → 1(r1(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
B(ql(0(x1))) → B(r0(x1))
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
B(ql(0(x1))) → B(r0(x1))
The value of delta used in the strict ordering is 4.
POL(r0(x1)) = x_1
POL(1(x1)) = 0
POL(m(x1)) = 0
POL(B(x1)) = x_1
POL(ql(x1)) = x_1
POL(qr(x1)) = 0
POL(b(x1)) = (2)x_1
POL(0(x1)) = 4 + x_1
POL(r1(x1)) = x_1
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
b(ql(1(x1))) → 1(b(r1(x1)))
r0(1(x1)) → 1(r0(x1))
r0(0(x1)) → 0(r0(x1))
r1(0(x1)) → 0(r1(x1))
r0(m(x1)) → m(r0(x1))
r1(m(x1)) → m(r1(x1))
r1(1(x1)) → 1(r1(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
r0(0(x1)) → 0(r0(x1))
r0(1(x1)) → 1(r0(x1))
r0(m(x1)) → m(r0(x1))
r1(0(x1)) → 0(r1(x1))
r1(1(x1)) → 1(r1(x1))
r1(m(x1)) → m(r1(x1))
r0(b(x1)) → qr(0(b(x1)))
r1(b(x1)) → qr(1(b(x1)))
0(qr(x1)) → qr(0(x1))
1(qr(x1)) → qr(1(x1))
m(qr(x1)) → ql(m(x1))
0(ql(x1)) → ql(0(x1))
1(ql(x1)) → ql(1(x1))
b(ql(0(x1))) → 0(b(r0(x1)))
b(ql(1(x1))) → 1(b(r1(x1)))